Nuprl Lemma : loc-ordered_wf
0,22
postcript
pdf
es
:ES,
L
:E List. loc-ordered(
es
;
L
)
Prop
latex
Definitions
ES
,
t
T
,
x
:
A
.
B
(
x
)
,
E
,
type
List
,
(
e
<loc
e'
)
,
x
,
y
.
t
(
x
;
y
)
,
l-ordered(
T
;
x
,
y
.
R
(
x
;
y
);
L
)
,
loc-ordered(
es
;
L
)
Lemmas
l-ordered
wf
,
es-locl
wf
,
es-E
wf
,
event
system
wf
origin
es:ES, L:E List. loc-ordered(es;L) 
Prop es:ES, L:E List. loc-ordered(es;L) Prop Tx:A. B(x)
x,y. t(x;y)